
import types

class all(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, all):
            return self.name == other.name
        else:
            return False
        
    def __repr__(self):
        return self.name

    def __iter__(self):
        return iter([])

class exist(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, exist):
            return self.name == other.name
        else:
            return False
        
    def __repr__(self):
        return self.name

    def __iter__(self):
        return iter([])

class variable(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, variable):
            return self.name == other.name
        else:
            return False
        
    def __repr__(self):
        return self.name

    def __iter__(self):
        return iter([])

class constant(object):
    def __init__(self, content):
        self.content = content
        
    def __eq__(self, other):
        if isinstance(other, constant):
            return self.content == other.content
        else:
            return False
        
    def __iter__(self):
        return iter([])
    
    def __repr__(self):
        return self.content

class function(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, function):
            return self.name == other.name
        else:
            return False
    
    def __repr__(self):
        return self.name
    
    def __iter__(self):
        return iter([])

class predicate(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, predicate):
            return self.name == other.name
        else:
            return False
    
    def __repr__(self):
        return self.name
    
    def __iter__(self):
        return iter([])

            
class clause:
    
    def __init__(self):
        self.P = predicate("P")
        self.Q = predicate("Q")
        self.R = predicate("R")
        self.f = function("f")
        self.v = variable("v") # used in rename
        self.u = variable("u") # used in rename
        self.w = variable("w") # used in rename
        self.a = constant("a")
        self.x = variable("x")
        self.y = variable("y")
        self.z = variable("z")
        self.A = all("A")
        self.E = exist("E")
        self.subCount = 0;
        self.subVar = [self.u,self.v,self.w]
        self.usedVar=[]
        self.exp1 = []
        self.exp2 = []
        #self.s=[self.y,'=>',self.x]
        self.s=[self.E,self.x,[[self.P,self.x],'&',[self.A,self.x,[[self.Q,self.x],'=>','~',[self.P,self.x]]]]]
#        self.s=['~',[self.A,self.x,[self.f,self.x]]]
        self.s=self.resolve(self.s,'<=>')
        print '-------------- <=> '
        print self.s
        self.s=self.resolve(self.s,'=>')
        print '-------------- => ',self.s
        print self.s
        self.s=self.resolve(self.s,'~')
        print '-------------- ~',self.s
        print self.s
        self.s=self.rename(self.s)
        print '-------------- rename',self.s
        #self.list = [[self.P,self.x],'|',[[self.Q,self.x],'&',[self.P,self.y]]]
        #self.list = [[[self.Q,self.x],'&',[self.P,self.y]],'|',[self.P,self.x]]
        #self.list = [[[self.P,self.x],'&',[self.P,self.y]],'|',[[self.P,self.x],'&',[self.Q,self.x],'&',[self.P,self.w]]]
        self.list = [[['~', [self.P, self.x]], '|', [self.Q, self.x], '&', [[self.Q, self.z], '&', [self.R, self.z, self.x]]], '&', [['~', [self.Q, self.x]], '|', ['~', [self.Q, self.z]], '|', ['~', [self.R, self.z, self.x]]], '&', ['~', [self.P, self.x]]]

        #self.list = [[self.P,self.x],'|',[[self.Q,self.x],'&',[self.Q,[self.f,self.x]],'&',[self.R,[self.f,self.x]]]]
        #self.list = [[self.P,self.x],'|',[[self.Q,self.x],'&',[self.R,self.x],'&',[self.Q,self.x]]]
        #self.extract_expression(self.list,'&')
        #self.list = self.findCon(self.list)
        #self.list = self.conjunction(self.list)
#        self.test = [['~', [self.P, self.x]], '|', [self.Q, self.x], '&', [[self.Q, self.z], '&', [self.R, self.z, self.x],'&',[self.R,self.x]]]
#        print self.test,'before and brackets'
        self.test = [['~', [self.P, self.x], '|', [self.Q, self.x], '&', [[self.Q, self.z], '&', [self.R, self.z, self.x]]], '&', ['~', [self.Q, self.x], '|', '~', [self.Q, self.z], '|', '~', [self.R, self.z, self.x]], '&', '~', [self.P, self.x]]
        self.test = self.notBrackets(self.test)
        self.test = self.removeNotBrackets(self.test)
        print self.test, 'self.test after remove bracketing not'
#        self.list = self.andBrackets(self.list)
#        print self.list,' and brackets'
#        self.list = self.conjunction(self.list)
#        print self.list,' conjunction'

        #print self.list,'the result'
        #self.exp1 = [self.P,self.x]
        #self.exp2 = [[self.Q,self.x],[self.R,self.x]]
        #self.s = self.conDis(self.exp1,self.exp2)
        print self.s
        
    def removeNotBrackets(self,list):
        added = False
        i = 0
        while True:
            print i,'i in loop'
           # print 'in loop with i',i,'len(list)',len(list)
            if added:
                i = i+1
                added = False
            while i<len(list) and isinstance(list[i],types.ListType) and len(list[i])==1 and isinstance(list[i][0],types.ListType) :
                list[i] = list[i][0]
            #print i,'current list',list,'list[i]',list[i],'len(list)',len(list)
            if i<len(list) and isinstance(list[i],types.ListType):
                list[i] = self.removeNotBrackets(list[i])
            if i<len(list) and isinstance(list[i],types.ListType) and list[i][0]=='~' and len(list[i])==2:
                list.insert(i, '~')
                list.insert(i+1,list[i+1][1])
                list.pop(i+2)
                added = True
            i = i+1
            if i>=len(list):
                break
        while i<len(list) and isinstance(list[i],types.ListType) and len(list[i])==1 and isinstance(list[i][0],types.ListType) :
                list[i] = list[i][0]
        return list
        
    def notBrackets(self,list):
        popped = False
        for i in xrange(0,len(list)):
            if popped:
                i=i-1
                popped = False
            while i<len(list) and isinstance(list[i],types.ListType) and len(list[i])==1 and isinstance(list[i][0],types.ListType) :
                list[i] = list[i][0]
            if i<len(list) and isinstance(list[i],types.ListType) and len(list[i])>2:
                list[i] = self.notBrackets(list[i])
            if i<len(list) and list[i]=='~' and i+1<len(list):
                list[i]=[list[i:i+2]]
                list.pop(i+1)
                popped = True
        for i in xrange(0,len(list)):
            while isinstance(list[i],types.ListType) and isinstance(list[i][0],types.ListType) and len(list[i])==1:
                    list[i] = list[i][0]
        return list
                
        
    def flatten(self,list,symbol):
#        print list
        new=[]
        for i in xrange(0,len(list)):
#            print '***',list[i]
            if isinstance(list[i],types.ListType) and not isinstance(list[i][0],(predicate,function)):
#                print 'is list'
                if symbol == '|':
                    new.extend(list[i])
                else:
                    new.extend(self.flatten(list[i],symbol))
            elif list[i]==symbol:
                new.append(symbol)
            elif list[i]=='|' and symbol=='&':
#                print 'in or list and symbol'
                new=[]
                new.append(list)
                break 
            else:
#                print 'else '
                new.append(list[i])
#        print 'new till now',new
        return new
    def oneContainsList(self,list):
        print list, 'in oneContainsList'
        if isinstance(list,types.ListType) and ('&' in list or '|' in list):
            theIn = '&'
            if '|' in list:
                theIn = '|'
            elif '&' in list:
                theIn = '&'
            print theIn,'theIn'
            for m in xrange(0,len(list)):
                if isinstance(list[m],types.ListType):
                    for n in xrange(0,len(list[m])):
                        if isinstance(list[m][n],types.ListType):
                            if '&' in list[m] and not theIn == '&':
                                return True
                            elif '|' in list[m] and not theIn=='|':
                                return True
        return False
    
#    what conjunction method does in notes form
#    
#    while(true)
#        if something or something
#            if both equal
#                remove one
#            else if one in any another
#                if another is anded
#                    remove the another
#                else if another is or'ed
#                    remove the one
#            else distribute or
#        else if something and something 
#            if both equal
#                remove one
#            else if one in any of the other
#                if other is anded        
#                    remove the one
#                else if other is or'ed
#                    remove the or'ed
#            else if one of them has an attribute that has an attribute that is list
#                repeat method on that attribute
#            else leave as it is
#                 break (return result)
    def andBrackets(self,list):
        toStartIndex = -1
        toEndIndex = -1
        for i in xrange(0,len(list)):
            while isinstance(list[i],types.ListType) and isinstance(list[i][0],types.ListType) and len(list[i])==1:
                list[i] = list[i][0]
            if isinstance(list[i],types.ListType) and '&' in list[i] and len(list[i])>3:
                list[i] = self.andBrackets(list[i])[0]
            if list[i] == '&' and toStartIndex == -1:
                toStartIndex = i-1
            elif i == len(list)-1 and not toStartIndex == -1:
                toEndIndex = len(list)
            elif list[i]=='|' and not toStartIndex == -1:
                toEndIndex = i-1
            if not toStartIndex == -1 and not toEndIndex == -1 and len(list)>3:
                list[toStartIndex] = [list[toStartIndex:toEndIndex]]
                popped = False
                numberOfPopped = 0
                for j in xrange(toStartIndex+1,toEndIndex):
                    if popped:
                        j = j-1
                        popped = False
                    if j<len(list):
                        numberOfPopped = numberOfPopped + 1
                        list.pop(j)
                        popped = True
                if numberOfPopped >2:
                    list.pop()
                toStartIndex = -1
                toEndIndex = -1
        for i in xrange(0,len(list)):
            while isinstance(list[i],types.ListType) and isinstance(list[i][0],types.ListType) and len(list[i])==1:
                    list[i] = list[i][0]
        return list
    
    def conjunction(self,list):
        counter = 0 
        breakOutside = False
        prevList = list
        #PUT BRACKETS AROUND THE ANDS
        list = self.andBrackets(list)
        while True:
            prevList = list
            while len(list)==1 and isinstance(list[0],types.ListType):
                list = list[0]
            print prevList,'prevList at start of loop'
            for i in xrange(0,len(list)):
                print i, 'counter 1st',list
                if i<len(list) and list[i] == '|':
                    print i,'index of |'
                    jIndex = 0
                    for j in xrange(i+1,len(list)):
                        if j<len(list) and list[j] == '|' and not i==j:
                            jIndex = j-1
                        elif j+1 == len(list) and list[j-1] == '|':
                            jIndex = j
                        print jIndex,'jIndex'
                        if( (list[j] == '|' and not i==j) or (j+1 == len(list) and list[j-1] == '|' )):
                            if list[i-1] == list[jIndex] and not jIndex == i-1:
                                list.pop(j)
                                list.pop(j-1)
                                if i>j:
                                    i = i-2
                                j = j-2
                                i = i-1
                            elif list[i-1] in list[jIndex]:
                                if '&' in list[jIndex] and not '|' in list[jIndex]:
                                    list.pop(j)
                                    list.pop(j-1)
                                    if i>j:
                                        i = i-2
                                    j = j-2
                                    i = i-1
                                elif '|' in list[jIndex] and not '&' in list[jIndex]:
                                    list.pop(i)
                                    list.pop(i-1)
                                    if j>i:
                                        j = j-2
                                    i = i-2
                                    i = i-1
                            elif list[jIndex] in list[i-1]:
                                if '&' in list[i-1] and not '|' in list[i-1]:
                                    list.pop(i)
                                    list.pop(i-1)
                                    if j>i:
                                        j = j-2
                                    i = i-2
                                    i = i-1
                                elif '|' in list[i-1] and not '&' in list[i-1]:
                                    list.pop(j)
                                    list.pop(j-1)
                                    if i>j:
                                        i = i-2
                                    j = j-2
                                    i = i-1
                            else:
                                list = self.findCon(list)
#                    if list==prevList:
#                        breakOutside = True
#                        break
                elif i<len(list) and list[i] == '&':
                    print i,'index of &'
                    jIndex = 0
                    for j in xrange(i+1,len(list)):
                        if j<len(list) and list[j] == '&' and not i==j:
                            jIndex = j-1
                        elif j+1 == len(list) and list[j-1] == '&':
                            jIndex = j
                        #elif (j-1)<len(list) and j+1 == len(list) and list[j-1] == '&':
                            #jIndex = j
                        print jIndex,'jIndex'
                        if ((j<len(list) and list[j] == '&' and not i==j) or (j+1 == len(list) and list[j-1] == '&' )):
                            print list[i-1], 'list[i-1]',list[jIndex],'list[jIndex]'
                            if list[i-1] == list[jIndex] and not jIndex == i-1:
                                list.pop(j)
                                list.pop(j-1)
                                if i>j:
                                    i = i-2
                                j = j-2
                                i = i-1
                                print 'checked equality'
                            elif list[i-1] in list[jIndex]:
                                if '|' in list[jIndex] and not '&' in list[jIndex]:
                                    list.pop(j)
                                    list.pop(j-1)
                                    if i>j:
                                        i = i-2
                                    i = i-2
                                    i = i-1
                                elif '&' in list[jIndex] and not '|' in list[jIndex]:
                                    list.pop(i)
                                    list.pop(i-1)
                                    if j>i:
                                        j = j-2
                                    i = i-2
                                    i = i-1
                            elif not isinstance(list[jIndex],types.ListType) and list[jIndex] in list[i-1]:
                                if '|' in list[i-1] and not '&' in list[i-1]:
                                    list.pop(j)
                                    list.pop(j-1)
                                    if i>j:
                                        i = i-2
                                    j = j-2
                                    i = i-1
                                elif '&' in list[i-1] and not '|' in list[i-1]:
                                    list.pop(i)
                                    list.pop(i-1)
                                    if j>i:
                                        j = j-2
                                    i = i-2
                                    i = i-1
                            elif self.oneContainsList(list[jIndex]):
                                list[jIndex] = self.conjunction(list[jIndex])
                                list = self.flatten(list,'&')
                                print list,'flattened'
                                print list[i-1],'before one containlist method call for list[i-1]'
                                if self.oneContainsList(list[i-1]):
                                    prevLength = len(list)
                                    prevJ = j
                                    list[i-1] = self.conjunction(list[i-1])
                                    j = prevJ
                                    if not len(list) == prevLength:
                                        i = i-(prevLength-len(list))
                                        j = j-(prevLength-len(list))
                                    print j,'the j after calling conj'
#                                    if self.oneContainsList(list[i-1]):
#                                        list[i-1] = self.conjunction(list[i-1])
                                    list = self.flatten(list,'&')
                                    print list,'flattened'
                            elif self.oneContainsList(list[i-1]):
                                prevLength = len(list)
                                prevJ = j
                                list[i-1] = self.conjunction(list[i-1])
                                j = prevJ
                                if not len(list) == prevLength:
                                    i = i-(prevLength-len(list))
                                    j = j-(prevLength-len(list))
                                print j,'the j after calling conj'
                                if self.oneContainsList(list[i-1]):
                                    list[i-1] = self.conjunction(list[i-1])
#                            else:
#                                breakOutside = True
#                                break
#                    if list==prevList:
#                        breakOutside = True
#                        break
            print prevList,'prevList at end of loop'
            if list == prevList:
                break
            else:
                print 'LLLLLLLLLLLLLLLLLLLLLLLLLLLL'
        return list  
    
    def equalList(self,l1,l2):
        while isinstance(l1,types.ListType) and len(l1) == 1:
            l1 = l1[0]
        while isinstance(l2,types.ListType) and len(l2) == 1:
            l2 = l2[0]
        return l1 == l2
    def distributeAnd(self,list):
        result = []
        print list,'in distributeAnd'
        for i in xrange(0,len(list)):
            if list[i]=='&':
                print list[i-1], 'in distributeAnd before change list[i-1]'
                print list[i+1], 'in distributeAnd before change list[i+1]'
                if '|' in list[i-1]:
                    if isinstance(list[i-1],types.ListType):
                        for j in xrange(0,len(list[i-1])):
                            if j<len(list[i-1]) and list[i-1][j]=='|':
                                list[i-1].pop(j)
                                j = j-1
                        if isinstance(list[i+1],types.ListType):
                            if j<len(list[i+1]) and list[i+1][j]=='|':
                                list[i+1].pop(j)
                                j = j-1
                        result = self.conDis(list[i+1],list[i-1],'&') 
                        print list[i+1], 'in distributeAnd list[i+1]'
                        print list[i-1], 'in distributeAnd list[i-1]'
                if '|' in list[i+1]:
                    print list[i-1],'list[i-1]'
                    print list[i+1],'list[i+1]'
                    if isinstance(list[i+1],types.ListType):
                        for j in xrange(0,len(list[i+1])):
                            if j<len(list[i+1]) and list[i+1][j]=='|':
                                list[i+1].pop(j)
                                j = j-1
                                print list[i+1],'in list i+1'
                        if isinstance(list[i-1],types.ListType):
                            for j in xrange(0,len(list[i-1])):
                                if j<len(list[i-1]) and list[i-1][j]=='|':
                                    list[i-1].pop(j)
                                    j = j-1
                                    print list[i-1],'in list i-1'
                        #result = self.conDis(list[i-1],list[i+1],'&')
        while '&' in result:
            result.remove('&')
        print result,'distributeAnd'
        result = self.findCon(result)
        return result
    
    def checkParentList(self,list):
        popped = False
        print list,'in checkParentList list'
        for i in xrange(0, len(list)):
            if i<len(list) and (list[i]=='|' or list[i]=='&'):
                if self.equalList(list[i-1],list[i+1]):
                    list.pop(i-1)
                    i = i-1
                    popped = True
                print list,'after checking equality'
                print list[i-1],'the list[i-1]',list[i+1],'the list[i+1]'
                if isinstance(list[i-1],types.ListType):
                    if isinstance(list[i-1][0],types.ListType):
                        while len(list[i-1]) == 1:
                            list[i-1] = list[i-1][0]
#                        for j in xrange(0,len(list[i-1])):
#                            if list[i+1] == list[i-1][j]:
#                                list.pop(i+1)
#                                popped = True
                        if list[i+1] in list[i-1]:
                            list.pop(i-1)
                            i = i-1
                            popped = True
                print list, 'after checking that the list[i+1] is in list[i-1]'
                if isinstance(list[i-1],types.ListType):
                    if isinstance(list[i+1][0],types.ListType):
                        while len(list[i+1]) == 1:
                            list[i+1] = list[i+1][0]
                        if list[i-1] in list[i+1]:
                            list.pop(i+1)
                            i = i-1
                            popped = True
                print list, 'after checking list[i-1] in list[i+1]'
                if popped:
                    for i in xrange(0,len(list)):
                        if i<len(list) and (list[i]=='|' or list[i]=='&'):
                            list.pop(i)
                            i = i-1
                            if i-1>0 and i+1<len(list) and list[i-1] == list[i+1]:
                                list.pop(i-1)
                                i = i-1
                    while len(list)==1:
                        list = list[0]
                    print list,'after removing |'
                    popped = False
#                    popped = True
#        if popped:
#            for i in xrange(0,len(list)):
#                if i<len(list) and list[i]=='|':
#                    list.pop(i)
#                    i = i-1
#            print list,'after removing &'
#        else:
#            return self.findCon(list)
        return list    
    def toCheckParent(self,result):
        for i in xrange(0,len(result)):
            if not result == None and i<len(result) and result[i]=='&':
                pre = len(result[i-1])
                result[i-1] = self.checkParentList(result[i-1])
                print result,'after checkparent result[i-1]'
#                if not pre == len(result[i-1]):
#                    result = self.findCon(result)
                if not result == None and not result[i+1]==None:
                    pre = len(result[i+1])
                    result[i+1] = self.checkParentList(result[i+1])
                    print result,'after checkparent result[i+1]'
                if isinstance(result[result.index('&')+1],types.ListType)and isinstance(result[result.index('&')+1][0],types.ListType) and isinstance(result[result.index('&')+1][0][0],types.ListType):
                    tempList = result[result.index('&')+1]
                    without = tempList
                    print tempList, 'tempList before adding &'
                    for i in xrange(0,len(tempList)):
                        if len(tempList[i])>1 and isinstance(tempList[i][0],types.ListType):
                            print tempList[i],'after if'
                            for j in xrange(1,len(tempList[i])):
                                tempList[i].insert(j, '&');
                                j = j+1
                    theIndex = result.index('&')
                    result[theIndex+1] = tempList
                    print tempList,'result[result.index(\'&\')+1] before',result[result.index('&')+1]
                    t = self.findCon(tempList)
                    print t, 't'
                    #result[result.index('&')+1] = self.findCon(tempList)
                    if result[result.index('&')+1] == []:
                        result.pop(result.index('&')+1)
                        result.pop(result.index('&'))
                    result[result.index(without)]=t
                    if result[result.index('&')+1] == []:
                        result.pop(result.index('&')+1)
                        result.pop(result.index('&'))
                    print result,'result[result.index(\'&\')+1] after',tempList
                    while isinstance(list,types.ListType) and '&' in list:
                        list.remove('&')
                    if len(result)>2 and '&' in result[2] and len(result[2])>1:
                        tempX = result[2]
                        for l in xrange(0,len(tempX)):
                            result.insert(len(result)-1,tempX[l])
                        result.pop()
        return result
        
    def findCon(self,list):
        result = []
        for i in xrange(0,len(list)):
            if list[i] == '|':
                if '&' in list[i-1]:
                    if isinstance(list[i-1],types.ListType):
#                        for j in xrange(0,len(list[i-1])):
#                            if j<len(list[i-1]) and list[i-1][j]=='&':
#                                list[i-1].pop(j)
#                                j = j-1
#                        if isinstance(list[i+1],types.ListType):
#                            if j<len(list[i+1]) and list[i+1][j]=='&':
#                                list[i+1].pop(j)
#                                j = j-1
                        result = self.conDis(list[i+1],list[i-1],'|') 
                if '&' in list[i+1]:
                    print list[i-1],'list[i-1]'
                    print list[i+1],'list[i+1]'
                    if isinstance(list[i+1],types.ListType):
#                        for j in xrange(0,len(list[i+1])):
#                            if j<len(list[i+1]) and list[i+1][j]=='&':
#                                list[i+1].pop(j)
#                                j = j-1
#                                print list[i+1],'in list i+1'
#                        if isinstance(list[i-1],types.ListType):
#                            for j in xrange(0,len(list[i-1])):
#                                if j<len(list[i-1]) and list[i-1][j]=='&':
#                                    list[i-1].pop(j)
#                                    j = j-1
#                                    print list[i-1],'in list i-1'
                        result = self.conDis(list[i-1],list[i+1],'|')
        #print result,'before calling checkParentList'
        #result = self.toCheckParent(result)
        
        return result
                    #self.findCon(list[:i-1].extend(result).extend(list[i+1:]))
    def extract_expression(self,list,symbol):
        return symbol in list
    
        
    def conDis(self,list1,list2,symbol):
        result = []
        print '1st list',list1,'2nd list',list2
        
        for e in list2:
            print e,'the e'
            if not e=='&' and symbol == '|':
                list1_temp = [list1]
                list1_temp.append('|')
                list1_temp.append(e)
                list1_temp = [list1_temp]
                result.extend(list1_temp)
                result.append('&')
                print result, 'in conDis'
            elif symbol == '&':
                list1_temp = [list1]
                list1_temp.append('&')
                list1_temp.append(e)
                list1_temp = [list1_temp]
                result.extend(list1_temp)
                result.append('|')
        result.pop()
        return result
                
    def move_not_inwards(self,s):
        print s
        a_imp=[]
        new=[]
        print 'move not inwards'
        for i in xrange(0,len(s)):
            if s[i] == '~':
                print "fond neg"
                new=s[:i]
                a_imp=s[i+1:]
                break
            else:
                a_imp=s
        print new
        print a_imp
        i=0
        while i <len(a_imp):
            
            print a_imp[i],i
            if isinstance(a_imp[i],types.ListType):
                if isinstance(a_imp[i][0],(predicate,function)):
                    new.append('~')
                    new.append(a_imp[i])
                else:
                    new.append(self.move_not_inwards(a_imp[i]))
                print 'out of list'          
            elif(isinstance(a_imp[i],exist)):
                print 'exist'
                new.append(self.A)
                new.append(a_imp[i+1])
                i=i+1
            elif(isinstance(a_imp[i],all)):
                print 'all'
                new.append(self.E)
                new.append(a_imp[i+1])
                i=i+1
                print i
            elif a_imp[i]=='&':
                print 'and'
                new.append('|')
            elif a_imp[i]=='|':
                print 'or'
                new.append('&')
            elif a_imp[i]=='~':
                'print not'
                new.append(a_imp[i+1:])
            else:
                print 'just add'
                new.append('~')
                new.append(a_imp[i])
                
            i=i+1            
            print 'till now new',new
        print 'final new',new
        return new
                        
    def eliminate_implications(self,s):
        print 'in elimination'
        b_imp=[]
        a_imp=[]
        print s
        for i in xrange(0,len(s)):
            if s[i] == '=>' or s[i] == '<=>':
                b_imp=s[:i]
                a_imp=s[i+1:]
        print b_imp
        print a_imp
        new = ['~']
        for b in b_imp:
            new.append(b)
        new.append('|')
        for a in a_imp:
            new.append(a)
        print new
        return new
        
    def renameVar(self,list,oldVar,newVar):
        print 'name var'
        for l in xrange(0,len(list)):
            if isinstance(list[l],variable) and list[l]==oldVar:
                list[l]=newVar
            elif isinstance(list[l],types.ListType):
                self.renameVar(list[l],oldVar,newVar)
        return list

    def search_replace(self,l,y,s):
        print 'in replace'
        print 'list is',s
        if s == l:
            print 'they are equal'
            s=y
        else:
            for i in xrange(0,len(s)):#z in s:
                print s[i],l
                if s[i] == l:
                    print s[i],l,'equal'
                    s[i]=y
                elif isinstance(s[i], types.ListType):
                    print 'is list'
                    self.search_replace(l,y,s[i])
        return s
        #search if a symbol is in the given list    
                
    def rename(self,list):
        print 'resolving',list
        for l in xrange(0,len(list)):
            
            if isinstance(list[l], types.ListType):
                print list[l],'is list'
                self.rename(list[l])
            elif isinstance(list[l],(exist,all)):
                print 'A or E'
                if list[l+1] in self.usedVar:
                    print 'repeated variable'
                    new = self.renameVar(list,list[l+1],self.subVar[self.subCount])
                    self.subCount=self.subCount+1
                    self.usedVar.append(self.subVar[self.subCount])
                    return self.search_replace(list,new,self.s)
                else:
                    self.usedVar.append(list[l+1])
        return self.s 
    
    def resolve(self,list,symbol):
        print 'resolving',list
        for l in xrange(0,len(list)):
            if isinstance(list[l], types.ListType):
                print list[l],'is list'
                self.resolve(list[l],symbol)
            elif list[l] == symbol:
                print 'is symbol'
                if symbol == '=>' or symbol == '<=>':
                    print 'is implication'
                    new=self.eliminate_implications(list)
                    return self.search_replace(list,new,self.s)
                if symbol == '~' and not isinstance(list[l+1][0],(variable, constant,predicate)):
                    print list[l+1][0]
                    print isinstance(list[l+1][0],(variable, constant,predicate))
                    print 'is negation'
                    new=self.move_not_inwards(list)
                    return self.search_replace(list,new[0],self.s)
        return self.s 
   
    #def distribute_and_over_or(s):
    #    """Given a sentence s consisting of conjunctions and disjunctions
    #    of literals, return an equivalent sentence in CNF.
    #    >>> distribute_and_over_or((A & B) | C)
    #    ((A | C) & (B | C))
    #    """
    #    if s.op == '|':
    #        s = NaryExpr('|', *s.args)
    #        if len(s.args) == 0:
    #            return FALSE
    #        if len(s.args) == 1:
    #            return distribute_and_over_or(s.args[0])
    #        conj = find_if((lambda d: d.op == '&'), s.args)
    #        if not conj:
    #            return NaryExpr(s.op, *s.args)
    #        others = [a for a in s.args if a is not conj]
    #        if len(others) == 1:
    #            rest = others[0]
    #        else:
    #            rest = NaryExpr('|', *others)
    #        return NaryExpr('&', *map(distribute_and_over_or,
    #                                  [(c|rest) for c in conj.args]))
    #    elif s.op == '&':
    #        return NaryExpr('&', *map(distribute_and_over_or, s.args))
    #    else:
    #        return s
   
    
if __name__ == "__main__":
    clause()
